T:Type, ll:(T List) List, x:T. (x  concat(ll))  (l:T List. (l  ll) & (x  l)) 

latex

Definitions	T, True, {T}, , AB, A, Y, nth_tl(n;as), if b t else f fi, ij, b, i<j, tl(l), reduce(f;k;as), A & B, hd(l), l[i], ||as||, x. t(x), as @ bs, concat(ll), Prop, t  T, P  Q, P  Q, P  Q, False, x:A. B(x), P & Q, x:A. B(x), P  Q, (x  l)
Lemmas	l member wf, iff wf, concat wf, append wf, false wf, nil member, and functionality wrt iff, exists functionality wrt iff, iff functionality wrt iff, all functionality wrt iff, cons member, member append, true wf, squash wf